the_es:ES, e:E.
isrcv(e)  snds(lnk(e), before(sender(e),index(e))) = msgs(lnk(e);before(e))  Msg List 

latex

Definitions

ES, t  T, x:A. B(x), lnk(e), msgs(l;before(e')), index(e), sender(e), snds(l, before(e,n)), Msg, ||as||, P  Q, isrcv(e), b, E, , AB, ij, False, A, sends(l;e), (Msg on l), {i..j}, Prop, P & Q, P  Q, S  T, P  Q, x:A. B(x), i  j < k, A & B, l[i], as @ bs, P  Q, {T}, SQType(T), True, T, IdLnk, before(e), (x  l), (e <loc e'), SqStable(P), , emsg(e), mapfilter(f;P;L), haslnk(l;e), rcvs(l;before(e')), filter(P;l), Top, b, Unit, null(as), Dec(P), x before y  l

Lemmas

or functionality wrt iff, l before-es-before, member append, cons member, l member wf, l before append, append assoc sq, top wf, non neg length, l before wf, assert of null, member exists, member map filter, null wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, filter append, map append sq, filter wf, es-haslnk wf, es-before wf, mapfilter wf, es-msg wf, sq stable from decidable, decidable assert, assert-es-haslnk, es-before-decomp, es-locl wf, member-es-before, es-msgs wf, length append, append wf, IdLnk wf, select wf, squash wf, true wf, es-axioms, last-es-snds-index, not functionality wrt iff, es-Msg wf, es-fifo-nil, length zero, es-snds-index wf, es-index wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-lnk wf, es-sender wf, assert wf, es-isrcv wf, es-E wf, le wf, nat properties, nat wf, event system wf